Nuprl Lemma : qmul-qdiv-cancel2
11,40
postcript
pdf
a
,
b
:
. (
(
a
= 0
))
(((
b
/
a
) *
a
) =
b
)
latex
Definitions
P
&
Q
,
P
Q
,
P
Q
,
,
t
T
,
P
Q
,
x
:
A
.
B
(
x
)
,
S
T
Lemmas
qmul-qdiv-cancel
,
qmul
com
,
qdiv
wf
,
int
inc
rationals
,
rationals
wf
,
not
wf
origin
a, b:
. (
(a = 0 
)) 
(((b/a) * a) = b) a, b:. ((a = 0 )) (((b/a) * a) = b) 
Q Q
T Qx:A. B(x)
T